Lean 4 入門メモ - Internet Explorer 2.0

Lean 4 入門メモ

ArchLinuxでelan-leanあるじゃんと思って入れたがなぜかlakeが入らなかったので，素直にインストールスクリプトでやるのがいい

$ curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh

namespaces / 名前空間

関数は．

namespace xで始めて，end xで囲った中でしか使えない

code:HelloLean.lean

namespace BasicFunctions

def pow2 x := x * x

-- Valid

#eval println! "valid {pow2 4}"

end BasicFunctions

-- BasicFunctions名前空間外なのでInvalid

#eval println! "valid {pow2 4}"

Function

第一級関数

以下関数fと自然数aを引数にとって

f(f(a))を返す

code:HelloLean.lean

def twice (f : Nat → Nat) (a : Nat) :=

f (f a)

記号的に縮約して関数を証明することが出来る

全ての自然数aについて操作+2を2回やると+4になることを証明している

$ f(x)=x+2, \forall a. f(f(a)) = a +4

code:HelloLean.lean

theorem twiceAdd2 (a : Nat) : twice (fun x => x + 2) a = a + 4 :=

rfl

·: \. || \centerdot

(· + 2)は(fun x => x + 2)と等しい（糖衣，即時関数）

code:Hello.lean

#eval twice (· + 2) 10

列挙型

#checkで名前空間に存在する用語の型を表示する

openで列挙型の名前空間に存在するものを展開する

パターンマッチがある

code: Hello.enum

inductive Weekday where

| sunday : Weekday

| monday : Weekday

| tuesday : Weekday

| wednesday : Weekday

| thursday : Weekday

| friday : Weekday

| saturday : Weekday

#check Weekday.sunday

#check Weekday.monday

-- Weekday名前空間にある用語を現在の名前空間へバラす

open Weekday

#check sunday

#check tuesday

-- パターンマッチ

-- バラした結果sundayなどだけでも通用していることに注意

def natOfWeekday (d : Weekday) : Nat :=

match d with

| sunday => 1

| monday => 2

| tuesday => 3

| wednesday => 4

| thursday => 5

| friday => 6

| saturday => 7

-- パターンマッチ，これはだいぶシンタクスシュガーがある

def isMonday : Weekday → Bool :=

fun

| monday => true

| _ => false

#eval isMonday sunday

#eval isMonday monday

def Weekday.next (d : Weekday) : Weekday :=

match d with

| sunday => monday

| monday => tuesday

| tuesday => wednesday

| wednesday => thursday

| thursday => friday

| friday => saturday

| saturday => sunday

def Weekday.previous : Weekday -> Weekday

| sunday => saturday

| monday => sunday

| tuesday => monday

| wednesday => tuesday

| thursday => wednesday

| friday => thursday

| saturday => friday

-- toStringを実装しないと出来ないことに注意

#eval Weekday.next Weekday.wednesday

#eval next wednesday

-- 全てのWeekday型のdに対して，昨日の明日は今日である

theorem Weekday.nextOfPrevious (d : Weekday) : next (previous d) = d :=

match d with

| sunday => rfl

| monday => rfl

| tuesday => rfl

| wednesday => rfl

| thursday => rfl

| friday => rfl

| saturday => rfl

-- あるいはこう書くことも出来る

theorem Weekday.nextOfPrevious' (d : Weekday) : next (previous d) = d := by

cases d -- A proof by case distinction

all_goals rfl -- Each case is solved using rfl

toString

自前で実装することも出来る

code:HelloLean.lean

-- "10"

#eval toString 10

-- "(10, 20)"

#eval toString (10, 20)

instance : ToString Weekday where

toString (d : Weekday) : String :=

match d with

| sunday => "Sunday"

| monday => "Monday"

| tuesday => "Tuesday"

| wednesday => "Wednesday"

| thursday => "Thursday"

| friday => "Friday"

| saturday => "Saturday"　

section, variable

code:VarSec

namespace Test1

def compose (α β γ: Type) (g : β → γ) (f : α → β) (x : α) : γ := g (f x)

def doTwice (α: Type) (h : α → α) (x: α) : α := h (h x)

def doThrice (α: Type) (h : α → α) (x: α) : α := h (h (h x))

end Test1

namespace Test2

variable (α β γ : Type)

def compose (g: β → γ) (f: α → β) (x: α) := g (f x)

def doTwice (h: α → α) (x: α) := h (h x)

def doThrice (h: α → α) (x : α) := h (h (h x))

end Test2

namespace Test3

variable (α β γ : Type)

variable (f: α → β) (h: α → α) (g: β → γ)

variable (x : α)

def compose := g (f x)

def doTwice := h (h x)

def doThrice := h (h (h x))

end Test3

-- 今namespaceで書いたがsectionで書くとこう

section useful

variable (α β γ : Type)

variable (g: β → γ) (f: α → β) (h: α → α)

variable (x: α)

def compose := g (f x)

def doTwice := h (h x)

def doThrice := h (h (h x))

end useful